R:Realizer. R-self-interface(R)  Prop 

latex

Definitions	Id, t  T, Knd, type List, True, Type, x.A(x), x:A. B(x), IdLnk, x. t(x), a:A fp B(a), x:AB(x), State(ds), DeclaredType(ds;x), x:AB(x), Void, P  Q, tag(k), IdDeq, f(x)?z, lnk(k), s = t, isrcv(k), b, Realizer, P & Q, x,y,z. t(x;y;z), x,y,z,w,v. t(x;y;z;w;v), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w. t(x;y;z;w), R-self-interface(R), Prop, lexpr{i}
Lemmas	es realizer ind wf, es realizer wf, assert wf, isrcv wf, lnk wf, subtype rel wf, fpf-cap wf, id-deq wf, tagof wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, true wf, Knd wf, Id wf